es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id} . e[e1,e2].True  e1 loc e2  

latex

Definitions	t  T, x:A. B(x), e loc e' , , True, e[e1,e2].P(e), P  Q, P  Q, b, False, A, loc(e), Id, E, x. t(x), P & Q, P  Q, ES, Trans(T;x,y.E(x;y)), A c B, x:A. B(x)
Lemmas	es-le-self, es-le-trans, event system wf, existse-between2 wf, true wf, es-E wf, Id wf, es-loc wf, es-loc-pred, es-le wf